COMMENT ⊗   VALID 00004 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	properties of allp
C00003 00003	proofs allp
C00005 00004	(proof somepprop)
C00006 ENDMK
C⊗;
;properties of allp
(wipe-out)
(get-proofs lispax prf ekl sys)

(proof allp)
;the following formulation of the definition of allp is more convenient when
;deriving instead of rewriting

(axiom |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)|)
(label allpfact)

(axiom |∀phi1 u.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
(label allp_introduction)

(axiom |∀phi1 x u.member(x,u)∧allp(phi1,u)⊃phi1(x)|)
(label allp_elimination)

(axiom |∀u a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|)
(label allp_implication)

(axiom |∀u.somep(phi1,u)≡(∃x.member(x,u)∧phi1(x))|)
(label somepfact)
(save-proofs allp)
;proofs allp

(proof allpprop)

;allpfact

(trw |∀phi x u.allp(phi,x.u)⊃phi(x)∧allp(phi,u)| (open allp))
;∀PHI X U.ALLP(PHI,X.U)⊃PHI(X)∧ALLP(PHI,U)

;allp_introduction

(ue (phi |λu.(∀y.member(y,u)⊃phi1(y))⊃allp(phi1,u)|)
    listinduction (open allp member) (use normal mode: always))
;∀U.(∀Y.MEMBER(Y,U)⊃PHI1(Y))⊃ALLP(PHI1,U)

;allp_elimination

(ue (phi |λu.member(x,u)∧allp(phi1,u)⊃phi1(x)|) listinduction 
    (part 1 (open member allp) (use normal mode: always)))
;∀U.MEMBER(X,U)∧ALLP(PHI1,U)⊃PHI1(X)

;allp_implication

(ue (phi |λu.∀a a1.allp(a,u)∧(∀x.a(x)⊃a1(x))⊃allp(a1,u)|) listinduction 
    (open allp))
;∀U A A1.ALLP(A,U)∧(∀X.A(X)⊃A1(X))⊃ALLP(A1,U)

(proof somepprop)

(ue (phi |λu.member(y,u)∧phi1(y)⊃somep(phi1,u)|)
    listinduction (open somep member) (use normal mode: always))
;∀U.MEMBER(Y,U)∧PHI1(Y)⊃SOMEP(PHI1,U)

(derive |∀u.(∃y.member(y,u)∧phi1(y))⊃somep(phi1,u)| *)

(ue (phi |λu.somep(phi1,u)⊃(∃x.member(x,u)∧phi1(x))|) listinduction 
    (part 1 (open member somep) (use normal mode: always) (der)))
;∀U.SOMEP(PHI1,U)⊃(∃X.MEMBER(X,U)∧PHI1(X))

(derive |∀u.somep(phi1,u)≡(∃x.member(x,u)∧phi1(x))| (* -2))